In math and physics, “linear” means “simple” and “non-linear” means “complicated”. The theory for solving linear equations is very well developed because it is simple enough to solve and only one solution exists. Non-linear equations can in general not be solved exactly (they have multiple solutions) and are the subject of much on-going research. Here is a brief description of how to distinguish a linear equation from a non-linear equation: In a linear equation, the variables (and their derivatives) must always appear as a simple first power. Here are some simple examples to illustrate this principle:
x+5=10 is linear and the equation is satisfied if and only if x takes the value 5. On the other hand, 5+x232 6 is non-linear because x2 is not a first power. The solution to this equation entails two values for x, namely −1 and +1 and this solution is harder to find than in the previous case.
In Boolean logic, equations have an analogous meaning but the operations of or (denoted ) and and (denoted ) replace the operations of plus (denoted +) and times (denoted ×), the connective ≡replaces the connective =, and Boolean variables can only take two values, namely true (also referred to as value 1) and false (also referred to as value 0), instead of any number as in the case of mathematics and physics. Analogously, non-linear Boolean equations are far harder to solve than linear Boolean equations and often, if there is one solution, there are many solutions.
There are two current competing methods for solving systems of non-linear Boolean equations. The first is via the use of Binary Decision Diagrams (BDDs). The second, is via Conjunctive Normal Form (CNF) Satisfiability checkers, e.g., POSIT, GRASP, zCHAFF, SATO, WALKSAT, etc. A BDD is intended as a compact representation of a Boolean function. A Boolean function has several input variables and one output variable. Every input variable may either be independently assigned value 0 or 1 or may be left unassigned. The output takes either value 0 or 1 or has undetermined value depending on the values assigned to the input variables. The input assignment patterns causing the output to have value 0 or 1 or undetermined may be listed in a table called a truth table. A truth table corresponds uniquely to a particular Boolean function.
A BDD is a mathematical abstraction which describes a truth table in an alternative and compact form. A BDD consists of a number of nodes, one distinguished as the root, one as the 0 node and one as the 1 node, representing function variable values, and arcs leading away from nodes, except the 0 and 1 nodes, representing values given to input variables. In this formalism 0 represents false and 1 represents true. The 0 and 1 nodes together represent the 0 and 1 values, respectively, which the function may take. A path from root to the 1 node signifies an assignment of values to input variables which causes the function's output variable to have value true and a path to the 0 node signifies an assignment causing an output value of false. Principal attributes of BDDs leading to their wide use are: 1) a BDD can be a compact, efficiently computed representation for a Boolean function and 2) operations for combining BDDs, such as conjunction (the  operator), can be fairly efficient provided the number nodes in the resulting BDD is not great.
BDDs are typically applied to non-linear equations as follows. A non-linear equation is a Boolean function. Variables named in a non-linear equation are its input variables. Thus, each equation may be represented by a BDD. Solving a system of non-linear equations means finding an assignment of values to all variables named in the system which causes each equation to have value 1. An equation, which has value 1, due to an assignment, is satisfied by that assignment. Since a system of non-linear equations is a Boolean function, a system may be solved if its corresponding BDD can be computed. Starting from the easily computed BDDs for each equation and using the rich set of operations available to BDDs, a BDD solver combines BDDs until one is left: that which represents the entire system. If that point can be reached, the system is solved. Observe that purely BDD techniques involve no guessing and checking of assignments.
By contrast, Satisfiability checkers, or SAT solvers, solve a restricted class of non-linear Boolean equations referred to as CNF formulas (see below for a description) by guessing, checking, discarding, and guessing again input variable values until either all possible combinations are exhausted or until an assignment is found which satisfies all equations. A SAT solver starts with all variables unassigned and attempts to extend the set of currently assigned input variables, one at a time, until it can be determined that all equations are satisfied or that all possible assignments to remaining unassigned variables will not satisfy all equations. In the former case a satisfying solution to the system is found. In the latter case one or more of the last variables to be assigned are reassigned or unassigned and the search for satisfying extensions is continued. If all possible extensions from the starting case, where all variables are unassigned, fail to satisfy all equations then the SAT solver reports no satisfying solution is possible.
BDD solvers are limited in the size of problems that they can solve, e.g., hundreds of variables and thousands of equations, depending on the problem domain. The principle problem plaguing BDD solvers is that as BDDs are being combined, they can get extremely large before completion, even if the final BDD is very small.
SAT solvers can solve problems with tens of thousands of variables and hundreds of thousands of equations, depending again on the problem domain. However, good performance seems to depend heavily on search heuristics, which choose the order in which variables are assigned values. Heuristics pertain to a trial-and-error method of problem solving used when an algorithmic approach is impractical. But the management of highly intelligent heuristics requires a great deal of overhead using conventional data structures and high overhead cancels the potential gains offered by such heuristics.
BDD and SAT solvers have (separately) been applied to a variety of problems. Many of these are a subclass of a general class of expressions called Layered Boolean Formulas (LBF).
A formula is one of the LBF class of expressions if it is given as 1) a list F={f1, f2, . . . , fm} of m Boolean functions whose inputs are taken from a set V={v1, v2, . . . , vn} of n Boolean variables; and 2) a list O=<o1, o2, . . . , om> of m Boolean values, one for each function, which specify the values the functions' outputs need to have if the expression is considered satisfied. The problem that needs to be solved, given an LBF Ø, is to determine whether there exists a list of Boolean values <b1, b2, . . . , bn> which the variables of V can be set to (that is, variable vi takes value bi for all 1≦i≦n) to satisfy the expression Ø (that is, makes all function outputs of F consistent with O) and if such a list exists (called a solution) output one.
The LBF class of expressions includes Conjunctive Normal Form (CNF) formulas, some Quantified Boolean Formulas (QBF), and Trace formulas. In a CNF formula each Boolean function fi is a conjunction of Boolean variables and complemented Boolean variables (a complemented Boolean variable just has a value opposite that of its variable counterpart) and each oi is 1. For example, f1 might be expressed as v1v3v8 which is a conjunction of two variables and one complemented variable (v3) and has value 0 if v1 and v8 have value 0 and v3 has value 1; has value 1 if v1 or v8 have value 1 or v3 has value 0; and has undetermined value otherwise. Boolean functions in a Trace formula typically use the equivalence operator ≡ and a few other operators such as ite which means if-then-else. For example, f1 of a Trace formula might be expressed asv≡ite(v1, v2, v3);This function has value 0 if either
1) v1 and v3 have value 0 and v has value 1; or
2) v1 and v have value 0 and v3 has value 1; or
3) v1 and v2 have value 1 and v has value 0; or
4) v1 and v have value 1 and v2 has value 0.
It has value 1 if either
1) v1 and v3 have value 0 and v has value 0; or
2) v1 has value 0 and v3 and v have value 1; or
3) v1 and v2 have value 1 and v has value 1; or
4) v1 has value 1 and v2 and v have value 0.
It has undetermined value otherwise.
A QBF expression is more complicated. Instead of asking whether there exists a list of Boolean values that satisfy Ø, the problem is to ask whether, for every possible combination of values that some of the V variables can have, there exists some combination of values that the remaining V variables can have with the result that Ø is satisfied, and if so, what is one such combination of values.
Before the 1990s, Binary Decision Diagrams (or BDDs) were considered the best way to deal with LBFs arising from practical problems. Unfortunately, on real LBFs, the number of nodes of “intermediate” BDDs (those that are formed while combining BDDs) can get to be enormous before realizing the final BDD which solves the problem and which can be quite small.
An alternative is to convert the BDDs to a conjunction of clauses, that is expressions of the form s1 s2 s3, and solve the conjunction of all conjunctions of clauses using a SAT solver. Before the 1990s this was infeasible because SAT solvers performed a form of tree search, that is SAT solvers did not effectively remember and reuse what had been learned in early parts of the search process. This sharply contrasts with BDDs which reuse portions of paths leading to the 1 node and 0 node, respectively. But the 1990s saw major improvements in the design of SAT solvers including conflict resolution, a form of remembering learned facts which we call lemmas, lookahead for inferences, better search heuristics, and exploitation of problem symmetry to prune away large portions of the search space. With these improvements SAT solvers can now compete with and in some cases significantly exceed the performance of BDD tools.
Formulas such as these arise in a variety of formal verification problems including microprocessor verification, illegal transition checking, and interconnect synthesis, among others. Consider microprocessor verification first. A circuit for use in a computer or other electronic device is designed from a formal specification of its functionality. This specification is written in some human understandable form such as make a noise at noon on cloudy days only. But an implementation of this statement as a circuit must be in a machine understandable form involving input and output variables. For example, let time represent time-of-day, let weather represent a type of weather condition, let noise represent whether a noise is made. Then the circuit to build may be expressednoise≡(time=12:00)(weather=cloudy).
The output of this circuit has either logic value true or false depending on the values of its input variables, namely noise, time, and weather. For example, if input values are sunny for weather, 12:00 for time, and true for noise, then the circuit outputs false. Observe that a formal specification may also have a logic value of true or false depending on some conditions. For example, the specification above has value false if a noise is made on a sunny day. If a circuit is to function as expected, its output logic values must be consistent with the logic values of the associated specification for corresponding input variable/specification conditions, that is, the specification and the circuit design should be functionally equivalent.
The microprocessor verification problem is to prove, using a computer program, that a given formal specification is logically equivalent to a given circuit expression. This is accomplished by using a special language for writing specifications which can efficiently be transformed into a conjunction of logic expressions. To determine whether the conjunction of expressions, S, is functionally equivalent to a circuit design, D, the expressions representing D and S are combined as follows:(DS)(DS)
This equivalence expression always has value false if and only if D and S are functionally equivalent.
A SAT solver (computer program) checks all possible combinations of input values to see whether a given equivalence expression always has value false. But all SAT solvers operate on CNF formulas. Thus, equivalence expressions must be translated to CNF before being solved by a SAT solver. Translation has two undesirable side-effects: 1) the length of the equivalence expression in CNF may be much greater; 2) variables which are understood in the context of the equivalence expression may lose that property as they become scattered in the translation. Continuing with the above example, consider attempting to show thatnoise≡(time=12:00)(weather=cloudy)is equivalent tonoise≡ite(weather=cloudy, time=12:00, weather=cloudy)
The later expression may have come from the special formal specification language. Current solvers cannot directly deal with the equivalence expression. Rather, a straightforward translation of the equivalence expression to CNF might give(noise (time=12:00)(weather=cloudy))(noise (time=12:00)(weather=cloudy))(noise (time =12:00)(weather=cloudy))(noise (time=12:00)(weather=cloudy))(noise (time=12:00)(weather=cloudy))(noise (time=12:00)(weather=cloudy))(noise (time=12:00)(weather=cloudy))(noise (time=12:00)(weather=cloudy))
A SAT solver will take this expression as input and attempt to solve it by searching for a solution. Although this example omits some trivial simplifications that could result in a reduced translated expression (and that most SAT solvers perform), it illustrates that the approach used by SAT solvers when inputs are extremely large results in a complexity of the translated expression that is much greater than the original expression, variables tend to get scattered throughout the translated expression, and the relationship between variables becomes blurred.